Nuprl Lemma : interface-compatible-join2 11,40
A, B, C:Dsys.
A || B  interface-compatible(A;C)  interface-compatible(B;C)  interface-compatible(A  B;C) 
latex

Definitionst  T, P  Q, x:A. B(x), interface-compatible(A;B), A  B, MsgA, Id, A || B, Dsys
Lemmasinterface-compatible wf, m-sys-compatible wf, Id wf, msga wf, m-sys-join wf2, interface-compatible-join, interface-compatible-symmetry

origin